theory zircon
imports "zircon_DataStructure"
begin
section "common"
definition add_overflow :: "Memory ⇒ SIZE_T ⇒ bool" where
"add_overflow mem size_t ≡
if size_t > size mem then False
else True
"
definition newIdFromList :: "nat list ⇒ nat" where
"newIdFromList idList ≡ SOME newId. newId∈({(2::nat)..} - (set idList) )"
definition newKOID :: "State ⇒ KOID" where
"newKOID s ≡
let lst = object s in
newIdFromList lst"
definition newHandle :: "State ⇒ KOID ⇒ ZX_RIGHTS_T ⇒ Handle"where
"newHandle s koid zx_rights_t ≡
let newProcess = pid(current s);
newhandle = ⦇Kobject = koid, rights = zx_rights_t, process_bound = newProcess⦈
in newhandle
"
definition newJob :: "State ⇒ job ⇒ job" where
"newJob s parentjob ≡
let newid = newKOID s;
newhdl = newHandle s (jid parentjob) ZX_DEFAULT_JOB_RIGHTS;
newjob = ⦇jid = newid, parent_handle = newhdl,
zircon_DataStructure.job.child_job = [], pro_set = {}, rights = ZX_DEFAULT_JOB_RIGHTS⦈
in newjob
"
definition newThread :: "State ⇒ string ⇒ thread" where
"newThread s threadname ≡
let newid = newKOID s;
newhandle = newHandle s newid ZX_RIGHT_NONE;
defaultprio = DEFAULT_PRIORITY;
newthread = ⦇tid = newid, handle = newhandle, name = threadname, base_priority = defaultprio⦈
in newthread
"
definition Create_Memory :: "State ⇒ State × Memory × ZX_STATUS_T"where
"Create_Memory s ≡
let newMemory = ⦇first_addr = nowAddr s, size = DEFAULT_SIZE, ownership = pid(current s),
access = {pid(current s)}, allocated = True⦈;
newAddr = nowAddr s + DEFAULT_SIZE;
newlst = newMemory # memorylst s
in (s⦇nowAddr:=newAddr,memorylst:=newlst⦈,newMemory,ZX_OK)
"
definition newVMO :: "State ⇒ State × Handle × ZX_STATUS_T"where
"newVMO s ≡
let newMemory = fst(snd(Create_Memory s));
newhandle = newHandle s (first_addr newMemory) ZX_DEFAULT_VMO_RIGHTS
in (fst(Create_Memory s),newhandle,snd(snd(Create_Memory s)))
"
definition validate_ranged_resource :: "Handle ⇒ ZX_RSRC_KIND ⇒ Memory_Addr ⇒ Memory_Addr ⇒
ZX_STATUS_T"where
"validate_ranged_resource hdl kind low high ≡
ZX_OK
"
definition validate_resource_mmio :: "Handle ⇒ Memory_Addr ⇒ SIZE_T ⇒ ZX_STATUS_T"where
"validate_resource_mmio hdl base lngth ≡
if lngth < 1 ∨ (base + lngth) > UINT64_MAX then ZX_ERR_INVALID_ARGS
else validate_ranged_resource hdl ZX_RSRC_KIND_MMIO base (base+lngth-1)
"
section "definition"
definition sys_check_memory_access_right :: "State ⇒ FLAGS ⇒ Memory ⇒ SIZE_T ⇒ RET" where
"sys_check_memory_access_right s flags mem size_t ≡
if pid(current s) = 0 then TEE_ERROR_GENERIC
else
if add_overflow mem size_t = False then TEE_ERROR_ACCESS_DENIED
else
if ¬(flags = TEE_MEMORY_ACCESS_NONSECURE
∨ flags = TEE_MEMORY_ACCESS_SECURE) then TEE_ERROR_ACCESS_DENIED
else
if ¬(flags = TEE_MEMORY_ACCESS_SECURE
∨ flags = TEE_MEMORY_ACCESS_NONSECURE) then TEE_ERROR_ACCESS_DENIED
else TEE_SUCCESS
"
definition sys_job_create :: "State ⇒ options ⇒ job ⇒ State × ZX_STATUS_T"where
"sys_job_create s options parentjob ≡
if options ≠ 0 then (s,ZX_ERR_INVALID_ARGS)
else
let newJOB = newJob s parentjob;
newlst = newJOB # JobDispatcher (dispatcher s)
in (s⦇dispatcher:= (dispatcher s)⦇JobDispatcher:= newlst⦈⦈, ZX_OK)
"
definition sys_thread_create :: "State ⇒ options ⇒ string ⇒ State × ZX_STATUS_T" where
"sys_thread_create s options threadname ≡
if options ≠ 0 then (s,ZX_ERR_INVALID_ARGS)
else
let newTHREAD = newThread s threadname;
newlst = newTHREAD # ThreadDispatcher (dispatcher s)
in (s⦇dispatcher:= (dispatcher s)⦇ThreadDispatcher:= newlst⦈⦈,ZX_OK)
"
definition sys_task_kill ::"State ⇒ Handle ⇒ State × ZX_STATUS_T" where
"sys_task_kill s h ≡
let newlst = remove1 h (handlelst s)
in if find(λx::job.(jid x) = (Kobject h)) (JobDispatcher(dispatcher s)) ≠ None
then let JOB = (the (find(λx::job.(jid x) = (Kobject h)) (JobDispatcher(dispatcher s))));
newlst1 = remove1 JOB (JobDispatcher(dispatcher s))
in (s⦇dispatcher:= (dispatcher s)⦇JobDispatcher:=newlst1⦈,handlelst := newlst⦈,ZX_OK)
else
if find(λx::thread.(tid x) = (Kobject h)) (ThreadDispatcher(dispatcher s)) ≠ None
then let THREAD = (the (find(λx::thread.(tid x) = (Kobject h)) (ThreadDispatcher(dispatcher s))));
newlst1 = remove1 THREAD (ThreadDispatcher(dispatcher s))
in (s⦇dispatcher:= (dispatcher s)⦇ThreadDispatcher:=newlst1⦈,handlelst := newlst⦈,ZX_OK)
else
if find(λx::process.(pid x) = (Kobject h)) (ProcessDispatcher(dispatcher s)) ≠ None
then let PROCESS = (the (find(λx::process.(pid x) = (Kobject h)) (ProcessDispatcher(dispatcher s))));
newlst1 = remove1 PROCESS (ProcessDispatcher(dispatcher s))
in (s⦇dispatcher:= (dispatcher s)⦇ProcessDispatcher:=newlst1⦈,handlelst := newlst⦈,ZX_OK)
else (s,ZX_ERR_WRONG_TYPE)
"
definition sys_channel_create :: "State ⇒ options ⇒ Conditions ⇒ KOID ⇒ KOID ⇒ State × ZX_STATUS_T" where
"sys_channel_create s options policy out1 out2≡
if options ≠ 0 then (s,ZX_ERR_INVALID_ARGS)
else
if policy ≠ ZX_POL_NEW_CHANNEL then (s,ZX_ERR_ACCESS_DENIED )
else
let newid = newKOID s;
newhandle0 = newHandle s out1 ZX_DEFAULT_CHANNEL_RIGHTS;
newhandlelst = newhandle0 # (handlelst s);
s = s⦇handlelst := newhandlelst⦈;
newhandle1 = newHandle s out2 ZX_DEFAULT_CHANNEL_RIGHTS;
newhandlelst1 = newhandle1 # (handlelst s);
s = s⦇handlelst := newhandlelst1⦈;
newchannel = ⦇cid = newid, handle0 = newhandle0, handle1 = newhandle1⦈;
newchannelst = newchannel # (channelst s)
in (s⦇channelst:= newchannelst⦈,ZX_OK)
"
definition sys_thread_set_priority :: "State ⇒ PRIO ⇒ State × ZX_STATUS_T"where
"sys_thread_set_priority s prio ≡
if prio < LOWEST_PRIORITY ∨ prio > HIGHEST_PRIORITY then (s,ZX_ERR_INVALID_ARGS)
else let currenthread = hd (ThreadDispatcher(dispatcher s));
currenthread = currenthread⦇base_priority := prio⦈;
newlst = currenthread # (tl (ThreadDispatcher(dispatcher s)))
in (s⦇dispatcher:= (dispatcher s)⦇ThreadDispatcher:=newlst⦈⦈,ZX_OK)
"
definition sys_vmo_create_physical :: "State ⇒ Handle ⇒ Memory_Addr ⇒ SIZE_T ⇒State × ZX_STATUS_T" where
"sys_vmo_create_physical s hdl paddr size_t ≡
if validate_resource_mmio hdl paddr size_t ≠ ZX_OK then (s,validate_resource_mmio hdl paddr size_t)
else
if snd(snd(newVMO s)) ≠ ZX_OK then (fst(newVMO s),snd(snd(newVMO s)))
else let s = fst(newVMO s)
in (s,ZX_OK)
"
definition sys_vmo_create :: "State ⇒ options ⇒ State × ZX_STATUS_T" where
"sys_vmo_create s options ≡
if options ≠ 0 then (s,ZX_ERR_INVALID_ARGS)
else let s = fst(newVMO s);
newhandle = newHandle s (nowAddr s) ZX_DEFAULT_VMO_RIGHTS;
newlst = newhandle # handlelst s
in (s⦇handlelst:=newlst⦈,ZX_OK)
"
definition sys_vmo_set_cache_policy :: "State ⇒ vmo ⇒ Handle option ⇒ ZX_CACHE_POLICY ⇒ vmo × ZX_STATUS_T"where
"sys_vmo_set_cache_policy s vobj hdl cp≡
if hdl = None then (vobj,ZX_ERR_BAD_HANDLE)
else if the (cache_policy vobj) = ZX_CACHE_POLICY_CACHED ∨ Handle.rights (the hdl) ≠ ZX_RIGHT_MAP then (vobj,ZX_ERR_ACCESS_DENIED)
else if (memory vobj) = None then (vobj,ZX_ERR_NOT_SUPPORTED)
else if cache_policy vobj ≠ None then (vobj,ZX_ERR_BAD_STATE)
else (vobj⦇cache_policy := Some cp⦈,ZX_OK)
"
definition sys_handle_duplicate :: "State ⇒ Handle ⇒ ZX_RIGHTS_T ⇒ State × Handle" where
"sys_handle_duplicate s hdl zx_rights_t ≡
let newhandle = ⦇Kobject = Kobject hdl, rights = zx_rights_t, process_bound = process_bound hdl⦈;
newlst = newhandle # handlelst s
in (s⦇handlelst:=newlst⦈,newhandle)
"
definition sys_handle_replace :: "State ⇒ Handle ⇒ ZX_RIGHTS_T ⇒ State × Handle" where
"sys_handle_replace s hdl zx_rights_t ≡
let newhandle = ⦇Kobject = Kobject hdl, rights = zx_rights_t, process_bound = process_bound hdl⦈;
tmplst = remove1 hdl (handlelst s);
newlst = newhandle # tmplst
in (s⦇handlelst:=newlst⦈,newhandle)
"
definition sys_handle_close :: "State ⇒ Handle ⇒ State"where
"sys_handle_close s hdl ≡
let newlst = remove1 hdl (handlelst s)
in s⦇handlelst:=newlst⦈
"
definition sys_vmar_map :: "State ⇒ vmo ⇒ map_flags ⇒ Memory_Addr ⇒ SIZE_T ⇒ State × ZX_STATUS_T" where
"sys_vmar_map s v flags maddr size_t≡
if vmo.rights v ≠ ZX_RIGHT_MAP then (s,ZX_ERR_ACCESS_DENIED)
else
if flags ≠ ZX_VM_FLAG_PERM_READ
∧ flags ≠ ZX_VM_FLAG_PERM_WRITE
∧ flags ≠ ZX_VM_FLAG_PERM_EXECUTE
then (s,ZX_ERR_INVALID_ARGS)
else let newAddr = ⦇first_addr = maddr, size = size_t⦈;
newlst = newAddr # addr(current s)
in (s⦇current:=(current s)⦇addr:=newlst⦈⦈,ZX_OK)
"
definition sys_vmar_unmap :: "State ⇒ Memory_Addr ⇒ SIZE_T ⇒ State × ZX_STATUS_T"where
"sys_vmar_unmap s maddr size_t≡
let tmpaddr = ⦇first_addr = maddr,size = size_t⦈;
newlst = remove1 tmpaddr (addr(current s))
in (s⦇current:=(current s)⦇addr:=newlst⦈⦈,ZX_OK)
"
definition sys_futex_wait :: "State ⇒ State"where
"sys_futex_wait s ≡
s⦇futex := wait⦈
"
definition sys_futex_wake :: "State ⇒ State"where
"sys_futex_wake s ≡
s⦇futex := wake⦈
"
definition sys_object_wait_one :: "State ⇒ ZX_SIGNALS_T ⇒ Handle option ⇒ State × ZX_STATUS_T" where
"sys_object_wait_one s observed hdl≡
if observed ≠ ZX_SIGNAL_NONE ∨ observed ≠ ZX_USER_SIGNAL_ALL then (s,ZX_ERR_INVALID_ARGS)
else if hdl = None then (s,ZX_ERR_BAD_HANDLE)
else if Handle.rights (the hdl) ≠ ZX_RIGHT_READ then (s,ZX_ERR_ACCESS_DENIED)
else (s,ZX_OK)
"
end